fix(Security): pin the tree-based extractor and guard distinctShape arity - #1

* fix(blueprint): repair LaTeX/bibtex errors breaking blueprint PDF build

The docs workflow has failed on main since ~2026-07-10. Three defects in
blueprint/src caused latexmk to exit non-zero:

- hachi_subfield.tex: math ($\cong$, $\sigma_{-1}$, ...) in section/
  subsection titles reached hyperref's PDF-bookmark string, and \cong
  triggered a fatal "Improper alphabetic constant". Wrapped the math in
  \texorpdfstring{}{} with plain-text fallbacks.
- hachi_subfield.tex: undefined macro \inv in a lemma body. Rewrote as
  standard inverse notation.
- references.bib: duplicate @misc{NOZ26} entry made bibtex error out,
  leaving all citations unresolved. Removed the redundant copy.

`leanblueprint pdf` and `leanblueprint web` now both exit 0.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* ci(docs): replace hand-rolled blueprint pipeline with docgen-action

The docs workflow built the blueprint and API docs with a bespoke
xu-cheng/texlive-action invocation, a brittle `pygraphviz==1.14` pin, and
manual deploy assembly -- a setup that has broken repeatedly.

Replace it with the maintained leanprover-community/docgen-action, the
standard used by leanblueprint's own template and mathlib-adjacent blueprint
projects. It drives doc-gen4 through the isolated `docbuild` layout doc-gen4
recommends, installs pygraphviz robustly, builds the blueprint, runs
`checkdecls`, and deploys -- all without custom plumbing.

Also:
- Add a `pull_request` trigger. The action gates deploy/upload to `push`, so
  PRs now get a validation-only blueprint + checkdecls build. This would have
  caught the LaTeX/bibtex regression fixed in the previous commit before it
  reached main.
- ArkLib's static `home_page/` is published via `build-page: false` (no Jekyll
  needed); `references` points at `blueprint/src/references.bib`.
- Document the CI flow and blueprint LaTeX gotchas in the wiki.

Note: this drops scripts/inject_nav.py's cross-page nav injection, which had
no equivalent in the standard action.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* ci(docs): pin docs workflow actions to latest, Dependabot-trackable refs

- actions/checkout v5 -> v7 (latest; matches the rest of the repo's workflows)
- jlumbroso/free-disk-space v1.3.0 -> v1.3.1 (latest)
- leanprover/lean-action stays at v1.5.0 (latest)
- docgen-action stays SHA-pinned at current main HEAD (2026-06-07): it ships no
  tags/releases, so a SHA is the only immutable, Dependabot-trackable ref.

github-actions Dependabot is already configured (.github/dependabot.yml,
monthly), and tracks both the version tags and the docgen-action SHA pin.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* fix(blueprint): repair stale \lean{} references so checkdecls passes

The docs job now runs `lake exe checkdecls blueprint/lean_decls` via
docgen-action — a validation the old hand-rolled pipeline never ran.
It surfaced 21 `\lean{}` tags across 6 blueprint sources that no longer
resolve after VCVio/ArkLib refactors. `lean_decls` is regenerated from
these tags by `leanblueprint web` in CI, so the source .tex is the fix.

Renames / namespace fixes (declaration exists under a new name):
  InterleavedCode            -> Code.interleavedCodeSet
  smoothCode                 -> ReedSolomon.smoothCode
  constrainedCode            -> ReedSolomon.constrainedCode
  multiConstrainedCode       -> ReedSolomon.multiConstrainedCode
  proximityMeasure           -> ProximityGap.proximityMeasure
  proximityGap               -> ProximityGap.proximityGap
  emptySpec                  -> OracleSpec.emptySpec
  OracleSpec.OracleQuery     -> OracleQuery
  OracleComp.evalDist        -> evalDist
  loggingOracle/cachingOracle-> OracleSpec.loggingOracle/cachingOracle
  randomOracle               -> OracleSpec.randomOracle
  Folding.polyFold           -> Polynomial.FoldingPolynomial.polyFold

Commented out (declaration removed or not yet formalized; prose kept):
  singletonSpec (a notation, not a declaration)
  UniPoly, MlPoly (removed from ArkLib)
  CheckClaim.oracleReduction_completeness (commented out in source)
  Folding.{exists_unique_bivariate,degree_bound_bivariate,fold,folding}

Verified: `lake exe checkdecls` on the repointed names resolves cleanly
against the v4.31.0 ArkLib environment.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>